\begin{tabbing}
chain{-}consistent($f$;${\it chain}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:E(${\it Sys}$). no\_repeats(Id;${\it chain}$($e$)) \& (0 $<$ $\parallel$${\it chain}$($e$)$\parallel$) \& (loc($e$) $\in$ ${\it chain}$($e$)))\+
\\[0ex]\& ($\forall$$e$, ${\it e'}$:E(${\it Sys}$). ${\it chain}$($e$) $\subseteq$ ${\it chain}$(${\it e'}$) $\vee$ ${\it chain}$(${\it e'}$) $\subseteq$ ${\it chain}$($e$))
\\[0ex]\& (\=$\forall$$e$:E(${\it Sys}$).\+
\\[0ex](\=($\uparrow$($e$ $\in_{b}$ ${\it In}$))\+
\\[0ex]$\Rightarrow$ (loc($e$) = if ${\it isupdate}$(${\it In}$($e$)) then hd((${\it chain}$($e$))) else last(${\it chain}$($e$)) fi ))
\-\\[0ex]\& (\=($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$)))\+
\\[0ex]$\Rightarrow$ ($\neg$(loc($f$($e$)) = loc($e$)))
\\[0ex]$\Rightarrow$ \=(adjacent(Id;${\it chain}$($e$);loc($f$($e$));loc($e$))\+
\\[0ex]\& adjacent(Id;${\it chain}$($f$($e$));loc($f$($e$));loc($e$))))
\-\-\\[0ex]\& (\=($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$)))\+
\\[0ex]$\Rightarrow$ (loc($f$($e$)) = loc($e$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:E(${\it Sys}$). ($a$ $<$loc $e$) $\Rightarrow$ $a$ $\leq$loc $f$($e$) ))
\-\\[0ex]\& (($\uparrow$($e$ $\in_{b}$ ${\it Out}$)) $\Rightarrow$ (loc($e$) = last(${\it chain}$($e$)))))
\-\\[0ex]\& ($\forall$$e$, ${\it e'}$:E(${\it Sys}$). ($e$ $<$loc ${\it e'}$) $\Rightarrow$ ${\it chain}$(${\it e'}$) $\subseteq$ ${\it chain}$($e$))
\-
\end{tabbing}